es:ES, A, T:Type, X:AbsInterface(A), base:T, f:(TAT), e:E. local-state(f;base;X;e)  T 

latex

Definitions

local-state(f;base;X;e), Unit, , tt, p q, p  q, p  q, e = e', deq-member(eq;x;L), a = b, a = b, qeq(r;s), q_less(a;b), q_le(r;s), eq_atom$n(x;y), [d], a < b, x f y, a < b, null(as), x =a y, (i = j), i z j, i <z j, p =b q, P  Q, P & Q, b, , ff, , A, prior-state(f;base;X;e), X(e), strong-subtype(A;B), E(X), a:A fp B(a), f(a), e  X, if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), t.1, let x,y = A in B(x;y), left + right, x:A  B(x), x:A. B(x), P  Q, s = t, ES, Type, x:AB(x), AbsInterface(A), E, b, t  T

Lemmas

es-interface-val wf, subtype rel wf, es-E wf, es-E-interface wf, member wf, es-interface-val wf2, es-local-prior-state wf, bool wf, es-is-interface wf, assert wf, not wf, bnot wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, event system wf, es-interface wf